1  /-
  2  Copyright (c) 2019 Chris Hughes. All rights reserved.
  3  Released under Apache 2.0 license as described in the file LICENSE.
  4  Authors: Chris Hughes
  5  
  6  ## Lagrange's four square theorem
  7  
  8  The main result in this file is `sum_four_squares`,
  9  a proof that every natural number is the sum of four square numbers.
 10  
 11  # Implementation Notes
 12  
 13  The proof used is close to Lagrange's original proof.
 14  -/
 15  import data.zmod.basic field_theory.finite group_theory.perm.sign
src         └─────────────┘ └─────────────────┘ └────────────────────┘
 16  import data.int.parity
src         └─────────────┘
 17  
 18  open finset polynomial finite_field equiv
 19  
 20  namespace int
 21  
 22  lemma sum_two_squares_of_two_mul_sum_two_squares {m x y : ℤ} (h : 2 * m =  x^2 + y^2) :
id                                                                             
src                                                                               
typ                                                                            
 23    m = ((x - y) / 2) ^ 2 + ((x + y) / 2) ^ 2 :=
id                               
src                                   
typ                              
 24  have (x^2 + y^2).even, by simp [h.symm, even_mul],
src                            └────┘      └┘        
typ                            └────┘      └┘        
doc                            └────┘      └┘        
txt                            └────┘      └┘        
par                            └────┘      └┘        
pid                                      └┘        
 25  have hxaddy : (x + y).even, by simpa [pow_two] with parity_simps,
src                                 └─────┘       └─────────────────┘
typ                                 └─────┘       └─────────────────┘
doc                                 └─────┘       └─────────────────┘
txt                                 └─────┘       └─────────────────┘
par                                 └─────┘       └─────────────────┘
pid                                             └────────────────┘
 26  have hxsuby : (x - y).even, by simpa [pow_two] with parity_simps,
id                          └┘             └─────┘
src                         └┘      └─────┘└─────┘└─────────────────┘
typ                         └┘      └─────┘└─────┘└─────────────────┘
doc                                 └─────┘       └─────────────────┘
txt                                 └─────┘       └─────────────────┘
par                                 └─────┘       └─────────────────┘
pid                                             └────────────────┘
st                                 └────────────────────────────────┘
 27  have (x^2 + y^2) % 2 = 0, by simp [h.symm],
id                  
src                          └────┘      
typ                        └────┘└────┘
doc                               └────┘      
txt                               └────┘      
par                               └────┘      
pid                                         
st                               └────────────┘
 28  (domain.mul_left_inj (show (2*2 : ℤ) ≠ 0, from dec_trivial)).1 $
id    └─────────────────┘                        └─────────┘  
src   └─────────────────┘                        └─────────┘  
typ   └─────────────────┘                        └─────────┘  
doc   └─────────────────┘                           └─────────┘
 29  calc 2 * 2 * m = (x - y)^2 + (x + y)^2 : by rw [mul_assoc, h]; ring
id                                       └───────┘  
src                                       └──┘└───────┘└┘   └───┘
typ                                  └──┘└───────┘└┘  └───┘
doc                                              └──┘         └┘   └───┘
txt                                              └──┘         └┘   └───┘
par                                              └──┘         └┘   └───┘
pid                                                └┘         └┘       
st                                              └────────────┘└─┘└─────┘
 30  ... = (2 * ((x - y) / 2))^2 + (2 * ((x + y) / 2))^2 :
id                                        
src                                           
typ                                       
 31    by rw [int.mul_div_cancel' hxsuby, int.mul_div_cancel' hxaddy]
id            └─────────────────┘ └────┘  └─────────────────┘ └────┘
src       └──┘└─────────────────┘      └┘└─────────────────┘      └┘
typ       └──┘└─────────────────┘└────┘└┘└─────────────────┘└────┘└┘
doc       └──┘                         └┘                         └┘
txt       └──┘                         └┘                         └┘
par       └──┘                         └┘                         └┘
pid         └┘                         └┘                         
st       └─────────────────────────────┘└──────────────────────────┘
 32  ... = 2 * 2 * (((x - y) / 2) ^ 2 + ((x + y) / 2) ^ 2) :
id                                        
src                                           
typ                                       
 33    by simp [mul_add, _root_.pow_succ, mul_comm, mul_assoc, mul_left_comm]
id              └─────┘  └─────────────┘  └──────┘  └───────┘  └───────────┘
src       └────┘└─────┘└┘└─────────────┘└┘└──────┘└┘└───────┘└┘└───────────┘└─
typ       └────┘└─────┘└┘└─────────────┘└┘└──────┘└┘└───────┘└┘└───────────┘└─
doc       └────┘       └┘               └┘        └┘         └┘             └─
txt       └────┘       └┘               └┘        └┘         └┘             └─
par       └────┘       └┘               └┘        └┘         └┘             └─
pid                  └┘               └┘        └┘         └┘             
st       └────────────────────────────────────────────────────────────────────
 34  
src  
typ  
doc  
txt  
par  
pid  
st   
 35  lemma exists_sum_two_squares_add_one_eq_k {p : ℕ} (hp : p.prime) :
id                                                          └────┘
src                                                          └────┘
typ                                                         └────┘
doc                                                           └────┘
 36    ∃ (a b : ℤ) (k : ℕ), a^2 + b^2 + 1 = k * p ∧ k < p :=
id                                     
src                                        
typ                                    
 37  hp.eq_two_or_odd.elim (λ hp2, hp2.symm ▸ ⟨1, 0, 1, rfl, dec_trivial⟩) $ λ hp1,
id   └┘└────────────┘└───┘    └─┘  └─┘└───┘            └─┘  └─────────┘       └─┘
src    └────────────┘└───┘            └───┘            └─┘  └─────────┘
typ  └┘└────────────┘└───┘    └─┘  └─┘└───┘            └─┘  └─────────┘       └─┘
doc                                                          └─────────┘
 38  let ⟨a, b, hab⟩ := zmodp.sum_two_squares hp (-1) in
id   └─┘              └───────────────────┘ └┘  
src                     └───────────────────┘     
typ  └─┘              └───────────────────┘ └┘  
 39  have hab' : (p : ℤ) ∣ a.val_min_abs ^ 2 + b.val_min_abs ^ 2 + 1,
id                       └──────────┘      └──────────┘    
src                       └──────────┘      └──────────┘    
typ                      └──────────┘      └──────────┘    
doc                         └──────────┘        └──────────┘
 40    from (zmodp.eq_zero_iff_dvd_int hp _).1 $ by simpa [eq_neg_iff_add_eq_zero] using hab,
id           └───────────────────────┘ └┘                 └────────────────────┘        └─┘
src          └───────────────────────┘             └─────┘└────────────────────┘└──────┘
typ          └───────────────────────┘ └┘          └─────┘└────────────────────┘└──────┘└─┘
doc                                                 └─────┘                      └──────┘
txt                                                 └─────┘                      └──────┘
par                                                 └─────┘                      └──────┘
pid                                                                            └────┘
st                                                 └───────────────────────────────────────┘
 41  let ⟨k, hk⟩ := hab' in
id   └─┘           └──┘
typ  └─┘           └──┘
 42  have hk0 : 0 ≤ k, from nonneg_of_mul_nonneg_left
id                         └───────────────────────┘
src                        └───────────────────────┘
typ                        └───────────────────────┘
 43    (by rw ← hk; exact (add_nonneg (add_nonneg (pow_two_nonneg _) (pow_two_nonneg _)) zero_le_one))
id              └┘                     └────────┘                     └────────────┘     └─────────┘
src        └───┘    └────┘            └────────┘               └──┘ └────────────┘└───┘└─────────┘
typ        └───┘└┘  └────┘            └────────┘               └──┘ └────────────┘└───┘└─────────┘
doc        └───┘    └────┘                                     └──┘               └───┘           
txt        └───┘    └────┘                                     └──┘               └───┘           
par        └───┘    └────┘                                     └──┘               └───┘           
pid          └─┘                                              └──┘               └───┘           
st        └─────────────────────────────────────────────────────────────────────────────────────────┘
 44    (int.coe_nat_pos.2 hp.pos),
id      └─────────────┘  └┘└──┘
src     └─────────────┘    └──┘
typ     └─────────────┘  └┘└──┘
 45  ⟨a.val_min_abs, b.val_min_abs, k.nat_abs,
id     └──────────┘   └──────────┘   └──────┘
src    └──────────┘   └──────────┘   └──────┘
typ    └──────────┘   └──────────┘   └──────┘
doc    └──────────┘   └──────────┘
 46      by rw [hk, int.nat_abs_of_nonneg hk0, mul_comm],
id              └┘  └───────────────────┘ └─┘  └──────┘
src         └──┘  └┘└───────────────────┘   └┘└──────┘
typ         └──┘└┘└┘└───────────────────┘└─┘└┘└──────┘
doc         └──┘  └┘                        └┘        
txt         └──┘  └┘                        └┘        
par         └──┘  └┘                        └┘        
pid           └┘  └┘                        └┘        
st         └─────┘└─────────────────────────┘└────────┘
 47    lt_of_mul_lt_mul_left
id     └───────────────────┘
src    └───────────────────┘
typ    └───────────────────┘
 48      (calc p * k.nat_abs = a.val_min_abs.nat_abs ^ 2 + b.val_min_abs.nat_abs ^ 2 + 1 :
id                └──────┘    └──────────┘└──────┘      └──────────┘└──────┘    
src                └──────┘    └──────────┘└──────┘      └──────────┘└──────┘    
typ               └──────┘    └──────────┘└──────┘      └──────────┘└──────┘    
doc                             └──────────┘                └──────────┘
 49          by rw [← int.coe_nat_inj', int.coe_nat_add, int.coe_nat_add, nat.pow_two, nat.pow_two,
id                    └──────────────┘  └─────────────┘  └─────────────┘  └─────────┘  └─────────┘
src             └────┘└──────────────┘└┘└─────────────┘└┘└─────────────┘└┘└─────────┘└┘└─────────┘└─
typ             └────┘└──────────────┘└┘└─────────────┘└┘└─────────────┘└┘└─────────┘└┘└─────────┘└─
doc             └────┘                └┘               └┘               └┘           └┘           └─
txt             └────┘                └┘               └┘               └┘           └┘           └─
par             └────┘                └┘               └┘               └┘           └┘           └─
pid               └──┘                └┘               └┘               └┘           └┘           └─
st             └─────────────────────┘└───────────────┘└───────────────┘└───────────┘└───────────┘└─
 50            int.nat_abs_mul_self, int.nat_abs_mul_self, ← _root_.pow_two, ← _root_.pow_two,
id             └──────────────────┘  └──────────────────┘    └────────────┘    └────────────┘
src  ─────────┘└──────────────────┘└┘└──────────────────┘└──┘└────────────┘└──┘└────────────┘└─
typ  ─────────┘└──────────────────┘└┘└──────────────────┘└──┘└────────────┘└──┘└────────────┘└─
doc  ─────────┘                    └┘                    └──┘              └──┘              └─
txt  ─────────┘                    └┘                    └──┘              └──┘              └─
par  ─────────┘                    └┘                    └──┘              └──┘              └─
pid  ─────────┘                    └┘                    └──┘              └──┘              └─
st   ─────────────────────────────┘└────────────────────┘└────────────────┘└────────────────┘└─
 51            int.coe_nat_one, hk, int.coe_nat_mul, int.nat_abs_of_nonneg hk0]
id             └─────────────┘  └┘  └─────────────┘  └───────────────────┘ └─┘
src  ─────────┘└─────────────┘└┘  └┘└─────────────┘└┘└───────────────────┘   └─
typ  ─────────┘└─────────────┘└┘└┘└┘└─────────────┘└┘└───────────────────┘└─┘└─
doc  ─────────┘               └┘  └┘               └┘                        └─
txt  ─────────┘               └┘  └┘               └┘                        └─
par  ─────────┘               └┘  └┘               └┘                        └─
pid  ─────────┘               └┘  └┘               └┘                        
st   ────────────────────────┘└──┘└───────────────┘└─────────────────────────┘
 52        ... ≤ (p / 2) ^ 2 + (p / 2)^2 + 1 :
id                                
src  ─────┘                         
typ  ─────┘                       
doc  ─────┘
txt  ─────┘
par  ─────┘
pid  ─────┘
st   ─────┘
 53          add_le_add
id           └────────┘
src          └────────┘
typ          └────────┘
 54            (add_le_add
id              └────────┘
src             └────────┘
typ             └────────┘
 55              (nat.pow_le_pow_of_le_left (zmodp.nat_abs_val_min_abs_le _) _)
id                └───────────────────────┘  └──────────────────────────┘
src               └───────────────────────┘  └──────────────────────────┘
typ               └───────────────────────┘  └──────────────────────────┘
 56              (nat.pow_le_pow_of_le_left (zmodp.nat_abs_val_min_abs_le _) _))
id                └───────────────────────┘  └──────────────────────────┘
src               └───────────────────────┘  └──────────────────────────┘
typ               └───────────────────────┘  └──────────────────────────┘
 57            (le_refl _)
id              └─────┘
src             └─────┘
typ             └─────┘
 58        ... < (p / 2) ^ 2 + (p / 2)^ 2 + (p % 2)^2 + ((2 * (p / 2)^2 + (4 * (p / 2) * (p % 2)))) :
id                                                                    
src                                                                         
typ                                                                   
 59          by rw [hp1, nat.one_pow, mul_one];
id                  └─┘  └─────────┘  └─────┘
src             └──┘   └┘└─────────┘└┘└─────┘
typ             └──┘└─┘└┘└─────────┘└┘└─────┘
doc             └──┘   └┘           └┘       
txt             └──┘   └┘           └┘       
par             └──┘   └┘           └┘       
pid               └┘   └┘           └┘       
st             └──────┘└───────────┘└───────┘└─
 60            exact (lt_add_iff_pos_right _).2
id                    └──────────────────┘
src            └────┘ └──────────────────┘└─────
typ            └────┘ └──────────────────┘└─────
doc            └────┘                     └─────
txt            └────┘                     └─────
par            └────┘                     └─────
pid                                      └─────
st   ───────────────────────────────────────────
 61              (add_pos_of_nonneg_of_pos (nat.zero_le _) (mul_pos dec_trivial
id                └──────────────────────┘  └─────────┘     └─────┘ └─────────┘
src  ───────────┘ └──────────────────────┘ └─────────┘└──┘ └─────┘└─────────┘
typ  ───────────┘ └──────────────────────┘ └─────────┘└──┘ └─────┘└─────────┘
doc  ───────────┘                                     └──┘        └─────────┘
txt  ───────────┘                                     └──┘                   
par  ───────────┘                                     └──┘                   
pid  ───────────┘                                     └──┘                   
st   ───────────────────────────────────────────────────────────────────────────
 62                (nat.div_pos hp.two_le dec_trivial)))
id                  └─────────┘ └───────┘
src  ─────────────┘ └─────────┘└───────┘           └───
typ  ─────────────┘ └─────────┘└───────┘           └───
doc  ─────────────┘                                └───
txt  ─────────────┘                                └───
par  ─────────────┘                                └───
pid  ─────────────┘                                └─┘
st   ────────────────────────────────────────────────────
 63        ... = p * p : begin
id                 
src  ─────┘        
typ  ─────┘        
doc  ─────┘
txt  ─────┘
par  ─────┘
pid  ─────┘
st   ─────┘              └─────
 64          conv_rhs { rw [← nat.mod_add_div p 2] },
id                            └─────────────┘ 
src          └─────────┘└────┘└─────────────┘ └──┘
typ          └─────────┘└────┘└─────────────┘└──┘
txt          └─────────┘└────┘                └──┘
par          └─────────┘└────┘                └──┘
pid                  └──────┘                └───┘
st   ─────────────────┘└───────────────────────┘  └┘
 65          simp only [nat.pow_two],
id                      └─────────┘
src          └─────────┘└─────────┘
typ          └─────────┘└─────────┘
doc          └─────────┘           
txt          └─────────┘           
par          └─────────┘           
pid              └──┘└┘           
st   ──────────────────────────────┘└─
 66          rw [← int.coe_nat_inj'],
id                 └──────────────┘
src          └────┘└──────────────┘
typ          └────┘└──────────────┘
doc          └────┘                
txt          └────┘                
par          └────┘                
pid            └──┘                
st   ─────────────────────────────┘└──
 67          simp only [nat.pow_two, int.coe_nat_add, int.coe_nat_mul, int.coe_nat_bit0, int.coe_nat_one,
id                      └─────────┘  └─────────────┘  └─────────────┘  └──────────────┘  └─────────────┘
src          └─────────┘└─────────┘└┘└─────────────┘└┘└─────────────┘└┘└──────────────┘└┘└─────────────┘└─
typ          └─────────┘└─────────┘└┘└─────────────┘└┘└─────────────┘└┘└──────────────┘└┘└─────────────┘└─
doc          └─────────┘           └┘               └┘               └┘                └┘               └─
txt          └─────────┘           └┘               └┘               └┘                └┘               └─
par          └─────────┘           └┘               └┘               └┘                └┘               └─
pid              └──┘└┘           └┘               └┘               └┘                └┘               └─
st   ─────────────────────────────────────────────────────────────────────────────────────────────────────
 68            two_mul, mul_add, add_mul],
id             └─────┘  └─────┘  └─────┘
src  ─────────┘└─────┘└┘└─────┘└┘└─────┘
typ  ─────────┘└─────┘└┘└─────┘└┘└─────┘
doc  ─────────┘       └┘       └┘       
txt  ─────────┘       └┘       └┘       
par  ─────────┘       └┘       └┘       
pid  ─────────┘       └┘       └┘       
st   ───────────────────────────────────┘└─
 69          ring,
src          └──┘
typ          └──┘
doc          └──┘
txt          └──┘
par          └──┘
st   ───────────┘└─
 70        end)
st   ────────┘
 71      (show 0 ≤ p, from nat.zero_le _)⟩
id                       └─────────┘
src                       └─────────┘
typ                      └─────────┘
 72  
 73  end int
 74  
 75  namespace nat
 76  
 77  open int
 78  
 79  open_locale classical
 80  
 81  private lemma sum_four_squares_of_two_mul_sum_four_squares {m a b c d : ℤ}
id                                                                           
src                                                                          
typ                                                                          
 82    (h : a^2 + b^2 + c^2 + d^2 = 2 * m) : ∃ w x y z : ℤ, w^2 + x^2 + y^2 + z^2 = m :=
id                                                     
src                                                            
typ                                                    
 83  have ∀ f : fin 4 → zmod 2, (f 0)^2 + (f 1)^2 + (f 2)^2 + (f 3)^2 = 0 →
id              └─┘    └──┘                               
src             └─┘     └──┘                                   
typ             └─┘    └──┘                               
 84      ∃ i : (fin 4), (f i)^2 + f (swap i 0 1)^2 = 0 ∧ f (swap i 0 2)^2 + f (swap i 0 3)^2 = 0,
id             └─┘            └──┘              └──┘           └──┘        
src            └─┘               └──┘                └──┘             └──┘         
typ            └─┘            └──┘              └──┘           └──┘        
doc                                  └──┘                   └──┘               └──┘
st           
 85    from dec_trivial,
id          └─────────┘
src         └─────────┘
typ         └─────────┘
doc         └─────────┘
 86  let f : fin 4 → ℤ := vector.nth (a::b::c::d::vector.nil) in
id           └─┘        └────────┘  └┘└┘└┘└┘└────────┘
src          └─┘         └────────┘   └┘ └┘ └┘ └┘└────────┘
typ          └─┘        └────────┘  └┘└┘└┘└┘└────────┘
 87  let ⟨i, hσ⟩ := this (coe ∘ f) (by rw [← @zero_mul (zmod 2) _ m, ← show ((2 : ℤ) : zmod 2) = 0, from rfl,
id   └─┘           └──┘  └─┘               └──────┘  └──┘                          └──┘             └─┘
src                       └─┘         └────┘ └──────┘ └──┘└────┘ └──┘      └──┘ └──┘└──┘└──┘└───────┘└─┘└─
typ  └─┘           └──┘  └─┘        └────┘ └──────┘ └──┘└────┘└──┘      └──┘ └──┘└──┘└──┘└───────┘└─┘└─
doc                                    └────┘              └────┘ └──┘      └──┘ └──┘    └──┘ └───────┘   └─
txt                                    └────┘              └────┘ └──┘      └──┘ └──┘    └──┘ └───────┘   └─
par                                    └────┘              └────┘ └──┘      └──┘ └──┘    └──┘ └───────┘   └─
pid                                      └──┘              └────┘ └──┘      └──┘ └──┘    └──┘ └───────┘   └─
st                                    └───────────────────────────┘└───────────────────────────────────────┘└─
 88    ← int.cast_mul, ← h]; simp only [int.cast_add, int.cast_pow]; refl) in
id       └──────────┘                  └──────────┘  └──────────┘
src  ───┘└──────────┘└──┘   └─────────┘└──────────┘└┘└──────────┘  └──┘
typ  ───┘└──────────┘└──┘  └─────────┘└──────────┘└┘└──────────┘  └──┘
doc  ───┘            └──┘   └─────────┘            └┘              └──┘
txt  ───┘            └──┘   └─────────┘            └┘              └──┘
par  ───┘            └──┘   └─────────┘            └┘              └──┘
pid  ───┘            └──┘       └──┘└┘            └┘            
st   ───────────────┘└───┘└────────────────────────────────────────────┘
 89  let σ := swap i 0 in
id           └──┘
src           └──┘
typ          └──┘
doc           └──┘
 90  have h01 : 2 ∣ f (σ 0) ^ 2 + f (σ 1) ^ 2,
id                                 
src                                    
typ                                
 91    from (@zmod.eq_zero_iff_dvd_int 2 _).1 $ by simpa [σ] using hσ.1,
id            └──────────────────────┘                           └┘
src           └──────────────────────┘            └─────┘ └──────┘  └┘
typ           └──────────────────────┘            └─────┘└──────┘└┘└┘
doc                                                └─────┘ └──────┘  └┘
txt                                                └─────┘ └──────┘  └┘
par                                                └─────┘ └──────┘  └┘
pid                                                      └────┘  └┘
st                                                └───────────────────┘
 92  have h23 : 2 ∣ f (σ 2) ^ 2 + f (σ 3) ^ 2,
id                                 
src                                    
typ                                
 93    from (@zmod.eq_zero_iff_dvd_int 2 _).1 $ by simpa using hσ.2,
id            └──────────────────────┘                        └┘
src           └──────────────────────┘            └──────────┘  └┘
typ           └──────────────────────┘            └──────────┘└┘└┘
doc                                                └──────────┘  └┘
txt                                                └──────────┘  └┘
par                                                └──────────┘  └┘
pid                                                     └────┘  └┘
st                                                └───────────────┘
 94  let ⟨x, hx⟩ := h01 in let ⟨y, hy⟩ := h23 in
id   └─┘            └─┘    └─┘            └─┘
typ  └─┘            └─┘    └─┘            └─┘
 95  ⟨(f (σ 0) - f (σ 1)) / 2, (f (σ 0) + f (σ 1)) / 2, (f (σ 2) - f (σ 3)) / 2, (f (σ 2) + f (σ 3)) / 2,
id                                                                            
src                                                                                           
typ                                                                           
 96    begin
st     └─────
 97      rw [← int.sum_two_squares_of_two_mul_sum_two_squares hx.symm, add_assoc,
id             └────────────────────────────────────────────┘ └─────┘  └───────┘
src      └────┘└────────────────────────────────────────────┘└─────┘└┘└───────┘└─
typ      └────┘└────────────────────────────────────────────┘└─────┘└┘└───────┘└─
doc      └────┘                                                     └┘         └─
txt      └────┘                                                     └┘         └─
par      └────┘                                                     └┘         └─
pid        └──┘                                                     └┘         └─
st   ───────────────────────────────────────────────────────────────┘└─────────┘└─
 98        ← int.sum_two_squares_of_two_mul_sum_two_squares hy.symm,
id           └────────────────────────────────────────────┘ └─────┘
src  ───────┘└────────────────────────────────────────────┘└─────┘└─
typ  ───────┘└────────────────────────────────────────────┘└─────┘└─
doc  ───────┘                                                     └─
txt  ───────┘                                                     └─
par  ───────┘                                                     └─
pid  ───────┘                                                     └─
st   ─────────────────────────────────────────────────────────────┘└─
 99        ← domain.mul_left_inj (show (2 : ℤ) ≠ 0, from dec_trivial), ← h, mul_add, ← hx, ← hy],
id           └─────────────────┘                        └─────────┘       └─────┘    └┘    └┘
src  ───────┘└─────────────────┘      └──┘ └┘└───────┘└─────────┘└───┘ └┘└─────┘└──┘  └──┘  
typ  ───────┘└─────────────────┘      └──┘ └┘└───────┘└─────────┘└───┘└┘└─────┘└──┘└┘└──┘└┘
doc  ───────┘└─────────────────┘      └──┘ └┘ └───────┘└─────────┘└───┘ └┘       └──┘  └──┘  
txt  ───────┘                         └──┘ └┘ └───────┘           └───┘ └┘       └──┘  └──┘  
par  ───────┘                         └──┘ └┘ └───────┘           └───┘ └┘       └──┘  └──┘  
pid  ───────┘                         └──┘ └┘ └───────┘           └───┘ └┘       └──┘  └──┘  
st   ───────────────────────────────────────────────────────────────┘└───┘└───────┘└────┘└────┘└──
100      have : univ.sum (λ x, f (σ x)^2) = univ.sum (λ x, f x^2),
id                                        └──────┘       
src      └─────┘          └──┘    └─┘ └──────┘  └──┘   └┘
typ      └─────┘          └──┘   └─┘ └──────┘  └──┘  └┘
doc      └─────┘          └──┘     └─┘ └──────┘  └──┘   └┘
txt      └─────┘          └──┘     └─┘           └──┘   └┘
par      └─────┘          └──┘     └─┘           └──┘   └┘
pid      └───┘└┘          └──┘     └─┘           └──┘   └┘
st   ───────────────────────────────────────────────────────────┘└─
101      { conv_rhs { rw finset.sum_univ_perm σ } },
id                       └──────────────────┘ 
src        └─────────┘└─┘└──────────────────┘ └┘
typ        └─────────┘└─┘└──────────────────┘└┘
txt        └─────────┘└─┘                     └┘
par        └─────────┘└─┘                     └┘
pid                └───┘                     └┘
st   ─────┘└────────┘└─────────────────────────┘└┘
102      have fin4univ : (univ : finset (fin 4)).1 = 0::1::2::3::0, from dec_trivial,
id                        └──┘   └────┘  └─┘          └┘
src      └──────────────┘ └──┘└─┘└────┘ └─┘└─────┘ └┘└┘        └───┘
typ      └──────────────┘ └──┘└─┘└────┘ └─┘└─────┘ └┘└┘        └───┘
doc      └──────────────┘ └──┘└─┘└────┘    └─────┘ └┘└┘        └───┘
txt      └──────────────┘     └─┘          └─────┘ └┘          └───┘
par      └──────────────┘     └─┘          └─────┘ └┘          └───┘
pid      └───────────┘└─┘     └─┘          └─────┘ └┘          └───┘
st   ────────────────────────────────────────────────────────────┘└────────────────┘└─
103      simpa [finset.sum_eq_multiset_sum, fin4univ, multiset.sum_cons, f]
id              └────────────────────────┘  └──────┘  └───────────────┘  
src      └─────┘└────────────────────────┘└┘        └┘└───────────────┘└┘ └─
typ      └─────┘└────────────────────────┘└┘└──────┘└┘└───────────────┘└┘└─
doc      └─────┘                          └┘        └┘                 └┘ └─
txt      └─────┘                          └┘        └┘                 └┘ └─
par      └─────┘                          └┘        └┘                 └┘ └─
pid                                     └┘        └┘                 └┘ 
st   ───────────────────────────────────────────────────────────────────────
104    end⟩
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
105  
106  private lemma prime_sum_four_squares {p : ℕ} (hp : p.prime) :
id                                                     └────┘
src                                                     └────┘
typ                                                    └────┘
doc                                                      └────┘
107    ∃ a b c d : ℤ, a^2 + b^2 + c^2 + d^2 = p :=
id                             
src                               
typ                            
108  have hm : ∃ m < p, 0 < m ∧ ∃ a b c d : ℤ, a^2 + b^2 + c^2 + d^2 = m * p,
id                                                 
src                                                       
typ                                                
109    from let ⟨a, b, k, hk⟩ := exists_sum_two_squares_add_one_eq_k hp in
id          └─┘          └┘     └─────────────────────────────────┘ └┘
src                              └─────────────────────────────────┘
typ         └─┘          └┘     └─────────────────────────────────┘ └┘
110    ⟨k, hk.2, nat.pos_of_ne_zero $
id              └────────────────┘
src             └────────────────┘
typ             └────────────────┘
111      (λ hk0, by rw [hk0, int.coe_nat_zero, zero_mul] at hk;
id          └─┘         └─┘  └──────────────┘  └──────┘
src                 └──┘   └┘└──────────────┘└┘└──────┘└─────┘
typ         └─┘     └──┘└─┘└┘└──────────────┘└┘└──────┘└─────┘
doc                 └──┘   └┘                └┘        └─────┘
txt                 └──┘   └┘                └┘        └─────┘
par                 └──┘   └┘                └┘        └─────┘
pid                   └┘   └┘                └┘        └────┘
st                 └──────┘└────────────────┘└────────┘└───────
112        exact ne_of_gt (show a^2 + b^2 + 1 > 0, from add_pos_of_nonneg_of_pos
id               └──────┘                          └──────────────────────┘
src        └────┘└──────┘      └┘   └┘└─┘└───────┘└──────────────────────┘
typ        └────┘└──────┘     └┘  └┘└─┘└───────┘└──────────────────────┘
doc        └────┘               └┘   └┘ └─┘ └───────┘                        
txt        └────┘               └┘   └┘ └─┘ └───────┘                        
par        └────┘               └┘   └┘ └─┘ └───────┘                        
pid                            └┘   └┘ └─┘ └───────┘                        
st   ────────────────────────────────────────────────────────────────────────────
113          (add_nonneg (pow_two_nonneg _) (pow_two_nonneg _)) zero_lt_one) hk.1),
id            └────────┘                     └────────────┘     └─────────┘  └┘
src  ───────┘ └────────┘               └──┘ └────────────┘└───┘└─────────┘└┘  └┘
typ  ───────┘ └────────┘               └──┘ └────────────┘└───┘└─────────┘└┘└┘└┘
doc  ───────┘                          └──┘               └───┘           └┘  └┘
txt  ───────┘                          └──┘               └───┘           └┘  └┘
par  ───────┘                          └──┘               └───┘           └┘  └┘
pid  ───────┘                          └──┘               └───┘           └┘  └┘
st   ───────────────────────────────────────────────────────────────────────────┘
114      a, b, 1, 0, by simpa [_root_.pow_two] using hk.1⟩,
id                             └────────────┘        └┘
src                     └─────┘└────────────┘└──────┘  └┘
typ                     └─────┘└────────────┘└──────┘└┘└┘
doc                     └─────┘              └──────┘  └┘
txt                     └─────┘              └──────┘  └┘
par                     └─────┘              └──────┘  └┘
pid                                        └────┘  └┘
st                     └────────────────────────────────┘
115  let m := nat.find hm in
id           └──────┘ └┘
src           └──────┘
typ          └──────┘ └┘
116  let ⟨a, b, c, d, (habcd : a^2 + b^2 + c^2 + d^2 = m * p)⟩ := (nat.find_spec hm).snd.2 in
id   └─┘                                            └───────────┘ └┘ └─┘ 
src                                                       └───────────┘    └─┘ 
typ  └─┘                                            └───────────┘ └┘ └─┘ 
117  have hm0 : 0 < m, from (nat.find_spec hm).snd.1,
id                         └───────────┘ └┘ └─┘ 
src                         └───────────┘    └─┘ 
typ                        └───────────┘ └┘ └─┘ 
118  have hmp : m < p, from (nat.find_spec hm).fst,
id                        └───────────┘ └┘ └─┘
src                         └───────────┘    └─┘
typ                       └───────────┘ └┘ └─┘
119  m.mod_two_eq_zero_or_one.elim
id   └─────────────────────┘└───┘
src   └─────────────────────┘└───┘
typ  └─────────────────────┘└───┘
120    (λ hm2 : m % 2 = 0,
id                  
src                  
typ                 
121      let ⟨k, hk⟩ := (nat.dvd_iff_mod_eq_zero _ _).2 hm2 in
id       └─┘            └─────────────────────┘       └─┘
src                      └─────────────────────┘     
typ      └─┘            └─────────────────────┘       └─┘
122      have hk0 : 0 < k, from nat.pos_of_ne_zero $ λ _, by simp [*, lt_irrefl] at *,
id                             └────────────────┘                   └───────┘
src                            └────────────────┘           └───────┘└───────┘└────┘
typ                            └────────────────┘          └───────┘└───────┘└────┘
doc                                                          └───────┘         └────┘
txt                                                          └───────┘         └────┘
par                                                          └───────┘         └────┘
pid                                                              └──┘         └──┘
st                                                          └───────────────────────┘
123      have hkm : k < m, by rw [hk, two_mul]; exact (lt_add_iff_pos_left _).2 hk0,
id                              └┘  └─────┘          └─────────────────┘      └─┘
src                          └──┘  └┘└─────┘  └────┘ └─────────────────┘└────┘
typ                         └──┘└┘└┘└─────┘  └────┘ └─────────────────┘└────┘└─┘
doc                           └──┘  └┘         └────┘                    └────┘
txt                           └──┘  └┘         └────┘                    └────┘
par                           └──┘  └┘         └────┘                    └────┘
pid                             └┘  └┘                                  └────┘
st                           └─────┘└───────┘└───────────────────────────────────┘
124      false.elim $ nat.find_min hm hkm ⟨lt_trans hkm hmp, hk0,
id       └────────┘   └──────────┘ └┘ └─┘  └──────┘ └─┘ └─┘  └─┘
src      └────────┘   └──────────┘         └──────┘
typ      └────────┘   └──────────┘ └┘ └─┘  └──────┘ └─┘ └─┘  └─┘
125        sum_four_squares_of_two_mul_sum_four_squares
id         └──────────────────────────────────────────┘
src        └──────────────────────────────────────────┘
typ        └──────────────────────────────────────────┘
126          (show a^2 + b^2 + c^2 + d^2 = 2 * (k * p),
id                                        
src                                      
typ                                       
127            by rw [habcd, hk, int.coe_nat_mul, mul_assoc]; simp)⟩)
id                    └───┘  └┘  └─────────────┘  └───────┘
src               └──┘     └┘  └┘└─────────────┘└┘└───────┘  └──┘
typ               └──┘└───┘└┘└┘└┘└─────────────┘└┘└───────┘  └──┘
doc               └──┘     └┘  └┘               └┘           └──┘
txt               └──┘     └┘  └┘               └┘           └──┘
par               └──┘     └┘  └┘               └┘           └──┘
pid                 └┘     └┘  └┘               └┘         
st               └────────┘└──┘└───────────────┘└─────────┘└────┘
128    (λ hm2 : m % 2 = 1,
id                  
src                  
typ                 
129      if hm1 : m = 1 then ⟨a, b, c, d, by simp only [hm1, habcd, int.coe_nat_one, one_mul]⟩
id       └┘                                           └─┘  └───┘  └─────────────┘  └─────┘
src      └┘                                 └─────────┘   └┘     └┘└─────────────┘└┘└─────┘
typ      └┘                                └─────────┘└─┘└┘└───┘└┘└─────────────┘└┘└─────┘
doc                                          └─────────┘   └┘     └┘               └┘       
txt                                          └─────────┘   └┘     └┘               └┘       
par                                          └─────────┘   └┘     └┘               └┘       
pid                                              └──┘└┘   └┘     └┘               └┘       
st                                          └───────────────────────────────────────────────┘
130      else --have hm1 : 1 < m, from lt_of_le_of_ne hm0 (ne.symm hm1),
131        let mp : ℕ+ := ⟨m, hm0⟩ in
id         └─┘      └┘       └─┘
src        └─┘      └┘
typ        └─┘      └┘       └─┘
doc                 └┘
132        let w := (a : zmod mp).val_min_abs, x := (b : zmod mp).val_min_abs,
id                      └──┘ └┘ └─────────┘            └──┘ └┘ └─────────┘
src                      └──┘    └─────────┘             └──┘    └─────────┘
typ                     └──┘ └┘ └─────────┘            └──┘ └┘ └─────────┘
doc                              └─────────┘                     └─────────┘
133            y := (c : zmod mp).val_min_abs, z := (d : zmod mp).val_min_abs in
id                      └──┘ └┘ └─────────┘            └──┘ └┘ └─────────┘
src                      └──┘    └─────────┘             └──┘    └─────────┘
typ                     └──┘ └┘ └─────────┘            └──┘ └┘ └─────────┘
doc                              └─────────┘                     └─────────┘
134        have hnat_abs : w^2 + x^2 + y^2 + z^2 =
id                                    
src                                       
typ                                   
135            (w.nat_abs^2 + x.nat_abs^2 + y.nat_abs ^2 + z.nat_abs ^ 2 : ℕ),
id              └──────┘   └──────┘   └──────┘    └──────┘      
src              └──────┘    └──────┘    └──────┘     └──────┘      
typ             └──────┘   └──────┘   └──────┘    └──────┘      
136          by simp [_root_.pow_two],
id                    └────────────┘
src             └────┘└────────────┘
typ             └────┘└────────────┘
doc             └────┘              
txt             └────┘              
par             └────┘              
pid                               
st             └────────────────────┘
137        have hwxyzlt : w^2 + x^2 + y^2 + z^2 < m^2,
id                                    
src                                        
typ                                   
138          from calc w^2 + x^2 + y^2 + z^2
id                              
src                                 
typ                             
139              = (w.nat_abs^2 + x.nat_abs^2 + y.nat_abs ^2 + z.nat_abs ^ 2 : ℕ) : hnat_abs
id                  └──────┘   └──────┘   └──────┘    └──────┘          └──────┘
src                  └──────┘    └──────┘    └──────┘     └──────┘      
typ                 └──────┘   └──────┘   └──────┘    └──────┘          └──────┘
140          ... ≤ ((m / 2) ^ 2 + (m / 2) ^ 2 + (m / 2) ^ 2 + (m / 2) ^ 2 : ℕ) :
id                                                           
src                                                              
typ                                                          
141            int.coe_nat_le.2 $ add_le_add (add_le_add (add_le_add
id             └────────────┘    └────────┘  └────────┘  └────────┘
src            └────────────┘    └────────┘  └────────┘  └────────┘
typ            └────────────┘    └────────┘  └────────┘  └────────┘
142              (nat.pow_le_pow_of_le_left (zmod.nat_abs_val_min_abs_le _) _)
id                └───────────────────────┘  └─────────────────────────┘
src               └───────────────────────┘  └─────────────────────────┘
typ               └───────────────────────┘  └─────────────────────────┘
143              (nat.pow_le_pow_of_le_left (zmod.nat_abs_val_min_abs_le _) _))
id                └───────────────────────┘  └─────────────────────────┘
src               └───────────────────────┘  └─────────────────────────┘
typ               └───────────────────────┘  └─────────────────────────┘
144              (nat.pow_le_pow_of_le_left (zmod.nat_abs_val_min_abs_le _) _))
id                └───────────────────────┘  └─────────────────────────┘
src               └───────────────────────┘  └─────────────────────────┘
typ               └───────────────────────┘  └─────────────────────────┘
145              (nat.pow_le_pow_of_le_left (zmod.nat_abs_val_min_abs_le _) _)
id                └───────────────────────┘  └─────────────────────────┘
src               └───────────────────────┘  └─────────────────────────┘
typ               └───────────────────────┘  └─────────────────────────┘
146          ... = 4 * (m / 2 : ℕ) ^ 2 : by simp [_root_.pow_two, bit0, bit1, mul_add, add_mul]
id                                           └────────────┘  └──┘  └──┘  └─────┘  └─────┘
src                                     └────┘└────────────┘└┘└──┘└┘└──┘└┘└─────┘└┘└─────┘└─
typ                                    └────┘└────────────┘└┘└──┘└┘└──┘└┘└─────┘└┘└─────┘└─
doc                                         └────┘              └┘    └┘    └┘       └┘       └─
txt                                         └────┘              └┘    └┘    └┘       └┘       └─
par                                         └────┘              └┘    └┘    └┘       └┘       └─
pid                                                           └┘    └┘    └┘       └┘       
st                                         └────────────────────────────────────────────────────
147          ... < 4 * (m / 2 : ℕ) ^ 2 + ((4 * (m / 2) : ℕ) * (m % 2 : ℕ) + (m % 2 : ℕ)^2) :
id                                                                   
src  ───────┘                                                            
typ  ───────┘                                                        
doc  ───────┘
txt  ───────┘
par  ───────┘
pid  ───────┘
st   ───────┘
148            (lt_add_iff_pos_right _).2 (by rw [hm2, int.coe_nat_one, _root_.one_pow, mul_one];
id              └──────────────────┘             └─┘  └─────────────┘  └────────────┘  └─────┘
src             └──────────────────┘         └──┘   └┘└─────────────┘└┘└────────────┘└┘└─────┘
typ             └──────────────────┘         └──┘└─┘└┘└─────────────┘└┘└────────────┘└┘└─────┘
doc                                           └──┘   └┘               └┘              └┘       
txt                                           └──┘   └┘               └┘              └┘       
par                                           └──┘   └┘               └┘              └┘       
pid                                             └┘   └┘               └┘              └┘       
st                                           └──────┘└───────────────┘└──────────────┘└───────┘└─
149              exact add_pos_of_nonneg_of_pos (int.coe_nat_nonneg _) zero_lt_one)
id                     └──────────────────────┘  └────────────────┘    └─────────┘
src              └────┘└──────────────────────┘ └────────────────┘└──┘└─────────┘
typ              └────┘└──────────────────────┘ └────────────────┘└──┘└─────────┘
doc              └────┘                                           └──┘
txt              └────┘                                           └──┘
par              └────┘                                           └──┘
pid                                                              └──┘
st   ────────────────────────────────────────────────────────────────────────────┘
150          ... = m ^ 2 : by conv_rhs {rw [← nat.mod_add_div m 2]};
id                                          └─────────────┘ 
src                          └────────┘└────┘└─────────────┘ └─┘
typ                         └────────┘└────┘└─────────────┘└─┘
txt                           └────────┘└────┘                └─┘
par                           └────────┘└────┘                └─┘
pid                                   └─────┘                └──┘
st                           └─────────┘└──────────────────────┘  └┘
151            simp [-nat.mod_add_div, mul_add, add_mul, bit0, bit1, mul_comm, mul_assoc, mul_left_comm,
id                                     └─────┘  └─────┘  └──┘  └──┘  └──────┘  └───────┘  └───────────┘
src            └──────────────────────┘└─────┘└┘└─────┘└┘└──┘└┘└──┘└┘└──────┘└┘└───────┘└┘└───────────┘└─
typ            └──────────────────────┘└─────┘└┘└─────┘└┘└──┘└┘└──┘└┘└──────┘└┘└───────┘└┘└───────────┘└─
doc            └──────────────────────┘       └┘       └┘    └┘    └┘        └┘         └┘             └─
txt            └──────────────────────┘       └┘       └┘    └┘    └┘        └┘         └┘             └─
par            └──────────────────────┘       └┘       └┘    └┘    └┘        └┘         └┘             └─
pid                └─────────────────┘       └┘       └┘    └┘    └┘        └┘         └┘             └─
st   ────────────────────────────────────────────────────────────────────────────────────────────────────
152              _root_.pow_add],
id               └────────────┘
src  ───────────┘└────────────┘
typ  ───────────┘└────────────┘
doc  ───────────┘              
txt  ───────────┘              
par  ───────────┘              
pid  ───────────┘              
st   ──────────────────────────┘
153        have hwxyzabcd : ((w^2 + x^2 + y^2 + z^2 : ℤ) : zmod mp) =
id                                             └──┘ └┘  
src                                                └──┘     
typ                                            └──┘ └┘  
154            ((a^2 + b^2 + c^2 + d^2 : ℤ) : zmod mp),
id                                    └──┘ └┘
src                                   └──┘
typ                                   └──┘ └┘
155          by simp [w, x, y, z, pow_two],
id                            └─────┘
src             └────┘ └┘ └┘ └┘ └┘└─────┘
typ             └────┘└┘└┘└┘└┘└─────┘
doc             └────┘ └┘ └┘ └┘ └┘       
txt             └────┘ └┘ └┘ └┘ └┘       
par             └────┘ └┘ └┘ └┘ └┘       
pid                  └┘ └┘ └┘ └┘       
st             └─────────────────────────┘
156        have hwxyz0 : ((w^2 + x^2 + y^2 + z^2 : ℤ) : zmod mp) = 0,
id                                          └──┘ └┘  
src                                             └──┘     
typ                                         └──┘ └┘  
157          by rw [hwxyzabcd, habcd, int.cast_mul, show ((m : ℤ) : zmod mp) = (mp : zmod mp), from rfl,
src             └──┘
typ             └──┘
doc             └──┘
txt             └──┘
par             └──┘
pid               └┘
st             └───┘
158            int.cast_coe_nat, coe_coe, zmod.cast_self_eq_zero]; simp,
src                                                                └──┘
typ                                                                └──┘
doc                                                                └──┘
txt                                                                └──┘
par                                                                └──┘
st                                                               └────┘
159        let ⟨n, hn⟩ := (zmod.eq_zero_iff_dvd_int.1 hwxyz0) in
id         └─┘            └──────────────────────┘  └────┘
src                        └──────────────────────┘
typ        └─┘            └──────────────────────┘  └────┘
160        have hn0 : 0 < n.nat_abs, from int.nat_abs_pos_of_ne_zero (λ hn0,
id                        └──────┘       └────────────────────────┘    └─┘
src                       └──────┘       └────────────────────────┘
typ                       └──────┘       └────────────────────────┘    └─┘
161          have hwxyz0 : (w.nat_abs^2 + x.nat_abs^2 + y.nat_abs^2 + z.nat_abs^2 : ℕ) = 0,
id                          └──────┘   └──────┘   └──────┘   └──────┘      
src                          └──────┘    └──────┘    └──────┘    └──────┘      
typ                         └──────┘   └──────┘   └──────┘   └──────┘      
162            by rw [← int.coe_nat_eq_zero, ← hnat_abs]; rwa [hn0, mul_zero] at hn,
163          have habcd0 : (m : ℤ) ∣ a ∧ (m : ℤ) ∣ b ∧ (m : ℤ) ∣ c ∧ (m : ℤ) ∣ d,
id                                                             
src                                                                
typ                                                            
164            by simpa [add_eq_zero_iff_eq_zero_of_nonneg (pow_two_nonneg _) (pow_two_nonneg _),
165              nat.pow_two, w, x, y, z, zmod.eq_zero_iff_dvd_int] using hwxyz0,
166          let ⟨ma, hma⟩ := habcd0.1,     ⟨mb, hmb⟩ := habcd0.2.1,
id           └─┘  └┘          └────┘        └┘          └────┘ 
src                                                            
typ          └─┘  └┘          └────┘        └┘          └────┘ 
167              ⟨mc, hmc⟩ := habcd0.2.2.1, ⟨md, hmd⟩ := habcd0.2.2.2 in
id                └┘          └────┘      └┘          └────┘  
src                                                           
typ               └┘          └────┘      └┘          └────┘  
168          have hmdvdp : m ∣ p,
id                           
src                          
typ                          
169            from int.coe_nat_dvd.1 ⟨ma^2 + mb^2 + mc^2 + md^2,
id                  └─────────────┘                    
src                 └─────────────┘                    
typ                 └─────────────┘                    
170              (domain.mul_left_inj (show (m : ℤ) ≠ 0, from int.coe_nat_ne_zero_iff_pos.2 hm0)).1 $
id                └─────────────────┘                      └─────────────────────────┘  └─┘  
src               └─────────────────┘                       └─────────────────────────┘       
typ               └─────────────────┘                      └─────────────────────────┘  └─┘  
doc               └─────────────────┘
171                by rw [← habcd, hma, hmb, hmc, hmd]; ring⟩,
172          (hp.2 _ hmdvdp).elim hm1 (λ hmeqp, by simpa [lt_irrefl, hmeqp] using hmp)),
id            └┘    └────┘ └──┘  └─┘    └───┘
src                        └──┘
typ           └┘    └────┘ └──┘  └─┘    └───┘
173        have hawbxcydz : ((mp : ℕ) : ℤ) ∣ a * w + b * x + c * y + d * z,
id                            └┘                            
src                                                           
typ                           └┘                            
174          from zmod.eq_zero_iff_dvd_int.1 $ by rw [← hwxyz0]; simp; ring,
id                └──────────────────────┘
src               └──────────────────────┘
typ               └──────────────────────┘
175        have haxbwczdy : ((mp : ℕ) : ℤ) ∣ a * x - b * w - c * z + d * y,
id                            └┘                            
src                                                           
typ                           └┘                            
176          from zmod.eq_zero_iff_dvd_int.1 $ by simp; ring,
id                └──────────────────────┘
src               └──────────────────────┘
typ               └──────────────────────┘
177        have haybzcwdx : ((mp : ℕ) : ℤ) ∣ a * y + b * z - c * w - d * x,
id                            └┘                            
src                                                           
typ                           └┘                            
178          from zmod.eq_zero_iff_dvd_int.1 $ by simp; ring,
id                └──────────────────────┘
src               └──────────────────────┘
typ               └──────────────────────┘
179        have hazbycxdw : ((mp : ℕ) : ℤ) ∣ a * z - b * y + c * x - d * w,
id                            └┘                            
src                                                           
typ                           └┘                            
180          from zmod.eq_zero_iff_dvd_int.1 $ by simp; ring,
id                └──────────────────────┘
src               └──────────────────────┘
typ               └──────────────────────┘
181        let ⟨s, hs⟩ := hawbxcydz, ⟨t, ht⟩ := haxbwczdy, ⟨u, hu⟩ := haybzcwdx, ⟨v, hv⟩ := hazbycxdw in
id         └─┘           └───────┘            └───────┘            └───────┘            └───────┘
typ        └─┘           └───────┘            └───────┘            └───────┘            └───────┘
182        have hn_nonneg : 0 ≤ n,
id                            
src                           
typ                           
183          from nonneg_of_mul_nonneg_left
id                └───────────────────────┘
src               └───────────────────────┘
typ               └───────────────────────┘
184            (by erw [← hn]; repeat {try {refine add_nonneg _ _}, try {exact pow_two_nonneg _}})
185            (int.coe_nat_pos.2 hm0),
id              └─────────────┘  └─┘
src             └─────────────┘
typ             └─────────────┘  └─┘
186        have hnm : n.nat_abs < mp,
id                     └──────┘  └┘
src                    └──────┘ 
typ                    └──────┘  └┘
187          from int.coe_nat_lt.1 (lt_of_mul_lt_mul_left
id                └────────────┘   └───────────────────┘
src               └────────────┘   └───────────────────┘
typ               └────────────┘   └───────────────────┘
188            (by rw [int.nat_abs_of_nonneg hn_nonneg, ← hn, ← _root_.pow_two]; exact hwxyzlt)
189            (int.coe_nat_nonneg mp)),
id              └────────────────┘ └┘
src             └────────────────┘
typ             └────────────────┘ └┘
190        have hstuv : s^2 + t^2 + u^2 + v^2 = n.nat_abs * p,
id                                       └──────┘  
src                                      └──────┘ 
typ                                      └──────┘  
191          from (domain.mul_left_inj (show (m^2 : ℤ) ≠ 0, from pow_ne_zero 2
id                 └─────────────────┘                       └─────────┘
src                └─────────────────┘                        └─────────┘
typ                └─────────────────┘                       └─────────┘
doc                └─────────────────┘
192              (int.coe_nat_ne_zero_iff_pos.2 hm0))).1 $
id                └─────────────────────────┘  └─┘   
src               └─────────────────────────┘        
typ               └─────────────────────────┘  └─┘   
193            calc (m : ℤ)^2 * (s^2 + t^2 + u^2 + v^2) = ((mp : ℕ) * s)^2 + ((mp : ℕ) * t)^2 +
id                                               └┘             └┘          
src                                                                          
typ                                              └┘             └┘          
194                ((mp : ℕ) * u)^2 + ((mp : ℕ) * v)^2 :
id                   └┘             └┘        
src                                           
typ                  └┘             └┘        
195              by simp [mp]; ring
196            ... = (w^2 + x^2 + y^2 + z^2) * (a^2 + b^2 + c^2 + d^2) :
id                                               
src                                                  
typ                                              
197              by simp only [hs.symm, ht.symm, hu.symm, hv.symm]; ring
198            ... = _ : by rw [hn, habcd, int.nat_abs_of_nonneg hn_nonneg]; dsimp [mp]; ring,
199        false.elim $ nat.find_min hm hnm ⟨lt_trans hnm hmp, hn0, s, t, u, v, hstuv⟩)
id         └────────┘   └──────────┘ └┘ └─┘  └──────┘ └─┘ └─┘  └─┘              └───┘
src        └────────┘   └──────────┘         └──────┘
typ        └────────┘   └──────────┘ └┘ └─┘  └──────┘ └─┘ └─┘  └─┘              └───┘
200  
201  lemma sum_four_squares : ∀ n : ℕ, ∃ a b c d : ℕ, a^2 + b^2 + c^2 + d^2 = n
id                                                           
src                                                              
typ                                                          
202  | 0 := ⟨0, 0, 0, 0, rfl⟩
id                       └─┘
src                      └─┘
typ                      └─┘
203  | 1 := ⟨1, 0, 0, 0, rfl⟩
id                       └─┘
src                      └─┘
typ                      └─┘
204  | n@(k+2) :=
id         
src        
typ        
205  have hm : (min_fac n).prime := min_fac_prime dec_trivial,
id              └─────┘   └───┘     └───────────┘ └─────────┘
src             └─────┘   └───┘     └───────────┘ └─────────┘
typ             └─────┘   └───┘     └───────────┘ └─────────┘
doc             └─────┘   └───┘                   └─────────┘
206  have n / min_fac n < n := factors_lemma,
id           └─────┘         └───────────┘
src          └─────┘         └───────────┘
typ          └─────┘         └───────────┘
doc           └─────┘
207  let ⟨a, b, c, d, h₁⟩ := show ∃ a b c d : ℤ, a^2 + b^2 + c^2 + d^2 = min_fac n,
id   └─┘                                              └─────┘
src                                                           └─────┘
typ  └─┘                                              └─────┘
doc                                                                      └─────┘
208    from prime_sum_four_squares hm in
id          └────────────────────┘ └┘
src         └────────────────────┘
typ         └────────────────────┘ └┘
209  let ⟨w, x, y, z, h₂⟩ := sum_four_squares (n / min_fac n) in
id   └─┘                 └──────────────┘     └─────┘
src                                               └─────┘
typ  └─┘                 └──────────────┘     └─────┘
doc                                                └─────┘
210  ⟨(a * x - b * w - c * z + d * y).nat_abs,
id                            └─────┘
src                           └─────┘
typ                           └─────┘
211   (a * y + b * z - c * w - d * x).nat_abs,
id                            └─────┘
src                           └─────┘
typ                           └─────┘
212   (a * z - b * y + c * x - d * w).nat_abs,
id                            └─────┘
src                           └─────┘
typ                           └─────┘
213   (a * w + b * x + c * y + d * z).nat_abs,
id                            └─────┘
src                           └─────┘
typ                           └─────┘
214    begin
215      rw [← int.coe_nat_inj', ← nat.mul_div_cancel' (min_fac_dvd (k+2)), int.coe_nat_mul, ← h₁, ← h₂],
216      simp [nat.pow_two, int.coe_nat_add, int.nat_abs_mul_self'],
217      ring,
st           └─
218    end⟩
st   ────┘
219  
220  end nat